package jtg.optimizer;

import polyglot.ast.Do;
import soot.Body;
import soot.Local;
import soot.Unit;
import soot.UnitPatchingChain;
import soot.toolkits.graph.UnitGraph;
import soot.util.Chain;

import javax.rmi.CORBA.Util;
import javax.script.ScriptEngine;
import javax.script.ScriptEngineManager;
import javax.script.ScriptException;
import java.util.*;
import java.util.Collection;
import java.util.List;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

import soot.util.Chain;

/**
 * 优化器：反编译器优化，将结果转为正确的类型
 * e.g. ASCLL码转为字符/布尔值  double转为float
 * */
public class Optimizer {
    private Body body; //
    private List<Unit> path;
    private HashMap<String,String> varToVar;
    private HashMap<String,String> varToType;

//    private final static String regex = "\\$[^=]+=\\([^)]+\\)\\s*[^)]*";
    // 编译正则表达式
    private Pattern pattern = Pattern.compile("\\$[^=]+ = \\([^)]+\\) [^…]+");

    public Optimizer(Body body){
        this.body = body;
        buildHashMapVarToType();
    }

    private void buildHashMapVarToType() {
        varToType = new HashMap<>();
        varToVar = new HashMap<>();
        Chain<Local> bodyLocalChain = body.getLocals();
        String name = "";
        String type = "";
        for (Local local : bodyLocalChain){
            name = local.getName();
            type = local.getType().toString();
            if (name.startsWith("$"))
            {
                name = name.substring(1);
            }
            if (!varToType.containsKey(name))
                varToType.put(name,type);
            System.out.println(name+" "+type);
        }
    }
    private void buildHashMapVarToVar(List<Unit> path){
        varToVar.clear();
        for (Unit unit:path){
            String subPath = unit.toString();
            if (pattern.matcher(subPath).find())
            {
                String[] subPathList = subPath.split(" ");
                varToVar.put(subPathList[0].substring(1),subPathList[subPathList.length-1]);
            }
        }
    }

    public String resultOptimize(String testItem, List<Unit> path,String pathConstraint) {
        this.buildHashMapVarToVar(path);

        // 处理testItem（数据形式 c0=1 c1=2 c3=3）
        String[] testItemList = testItem.split(" ");
        String varName;        //变量名
        String varValue = "";  //变量值
        StringBuilder testInput = new StringBuilder(); //新的返回结果
        for (String s : testItemList) {
            String[] subItems = s.split("=");
            varName = subItems[0];
            varValue = subItems[1];
            if (varToType.get(varName).equals(ParameterType.CHAR)) {
                //如果是字符类型，将ASCLL码转为对应的字符
                int temp = Integer.parseInt(subItems[1]);
                if (temp == 0){
                    varValue = "'\\0'";
                }
                else
                    varValue = "'" + String.valueOf((char) temp) + "'";
            } else if (varToType.get(varName).equals(ParameterType.BOOLEAN)) {
                //如果是布尔值，将ASCLL码转为对应的布尔值
                int temp = Integer.parseInt(subItems[1]);
                if (temp == 0) varValue = "true";
                else varValue = "false";
            }
            else if (ParameterType.isNumber(varToType.get(varName))){
                if (varToVar.containsKey(varName)){
                    String curKey = varName;
                    while (varToVar.containsKey(curKey)){
                        curKey = varToVar.get(curKey);
                    }
                    if (!varToType.get(curKey).equals(varToType.get(varName)))
                    {
                        varValue = numTypeConversion(varValue,varToType.get(varName),varToType.get(curKey));
                    }
                }
            }
            testInput.append(" ").append(varName).append("=").append(varValue);
        }
        return testInput.toString();
    }

    /**
     * @param varValue 当前值;
     * @param type1 原来类型
     * @param type2 目标类型
     *
     * @return 目标类型对应的值
     * */
    //TODO 1.没有考虑到转换类型后是否越界 2.转换后是否仍然满足原来的约束(如浮点数转整型)
    private String numTypeConversion(String varValue, String type1, String type2) {
        // 创建JavaScript引擎
        ScriptEngineManager manager = new ScriptEngineManager();
        ScriptEngine engine = manager.getEngineByName("js");

        try {
            // 计算表达式
            Object result = engine.eval(varValue);

            switch (type2) {
                case ParameterType.INT:
                    // 将结果转换为整数
                    int intValue = ((Number) result).intValue();
                    varValue = String.valueOf(intValue);
                    break;
                case ParameterType.DOUBLE:
                    double doubleValue = ((Number) result).doubleValue();
                    varValue = String.valueOf(doubleValue);
                    break;
                case ParameterType.FLOAT:
                    float floatValue = ((Number) result).floatValue();
                    varValue = String.valueOf(floatValue);
                    break;
            }
        } catch (ScriptException e) {
            e.printStackTrace();
        }
        return varValue;
    }

    private String variableValueRange(String var,String type){
        String constraintUpper = "";
        String constraintLower = "";
        String minValue = "";
        String maxValue = "";
        switch (type){
            case "int":
                minValue = String.valueOf(Integer.MIN_VALUE);
                maxValue = String.valueOf(Integer.MAX_VALUE);
                break;
            case "long":
                minValue = String.valueOf(Long.MIN_VALUE);
                maxValue = String.valueOf(Long.MAX_VALUE);
                break;
            case "byte":
                minValue = String.valueOf(Byte.MIN_VALUE);
                maxValue = String.valueOf(Byte.MAX_VALUE);
                break;
            case "short":
                minValue = String.valueOf(Short.MIN_VALUE);
                maxValue = String.valueOf(Short.MAX_VALUE);
                break;
            case "float":
                minValue = String.valueOf(Float.MIN_VALUE);
                maxValue = String.valueOf(Float.MAX_VALUE);
                break;
            case "double":
                minValue = String.valueOf(Double.MIN_VALUE);
                maxValue = String.valueOf(Double.MAX_VALUE);
                break;
            default:
                throw new Error("缺少类型！");
        }
        constraintLower = "0-" +  var +  minValue + " <= 0" ;
        constraintUpper = var + "<=" + maxValue;
        return "( " + constraintLower + " && " + constraintUpper + " )";
    }

    private String  Rounding(String var,String varType,String condition){
        if (varType.equals("float")||varType.equals("double")){
            return condition;
        }
        else {
            if (condition.contains("<=")){
//                condition = condition.replace("2.5","2");
                return condition; //TODO 处理 <=
            }
            else if (condition.contains(">=")){
                return condition;//TODO 处理 >= 注*：要将>=转为<=的形式（z3不支持>/>=）
            }
            else if (condition.contains("=")){
                return Rounding(var,varType,condition.replace("=","<=")) +"&&"+
                        Rounding(var,varType,condition.replace("=",">="));
            }
            else if (condition.contains(">"))
            {
                return Rounding(var,varType,condition.replace(">",">="));
            }
            else if (condition.contains("<"))
            {
                return Rounding(var,varType,condition.replace("<","<="));
            }
            else {
                return condition; // TODO 更多处理
            }
        }
    }
    public String constraintOptimizer(ArrayList<String> stepConditions, List<Unit> path){
        buildHashMapVarToVar(path);
        System.out.println("map varToType:");
        System.out.println(varToType.toString());
        System.out.println("map varToVar:");
        System.out.println(varToVar.toString());

        for (String stepItem:stepConditions)
            System.out.println(stepItem);

        StringBuilder additionalConstraint = new StringBuilder();
        for (String item : varToVar.keySet()){
            for (int i = 0;i<stepConditions.size();i++){
                if (stepConditions.get(i).contains(item)){
                    stepConditions.set(i,Rounding(item,varToType.get(varToVar.get(item)),stepConditions.get(i)));
                }
            }
        }
        for (String item:varToVar.keySet()){
            if (additionalConstraint.length()>0)
                additionalConstraint.append("&&");
            additionalConstraint.append(variableValueRange(item,varToType.get(varToVar.get(item))));
        }
        System.out.println("additionalConstraint:");
        System.out.println(additionalConstraint.toString());
        StringBuilder result = new StringBuilder(additionalConstraint.toString());
        for (String stepCondition:stepConditions){
            if (result.toString().equals(""))
                result = new StringBuilder(stepCondition);
            else
                result.append(" && ").append(stepCondition);
        }
        return result.toString();
    }
}

